
@book{Church:1985,
 author = {Church, Alonzo},
 title = {The Calculi of Lambda Conversion. (AM-6) (Annals of Mathematics Studies)},
 year = {1985},
 isbn = {0691083940},
 publisher = {Princeton University Press},
 address = {Princeton, NJ, USA},
} 
@book{heyting1930formalen,
  title={Die formalen Regeln der intuitionistischen Logik},
  author={Heyting, A.},
  series={Sitzungsberichte der Preussischen Akademie der Wissenschaften. Physikalisch-mathematische Klasse},
  url={http://books.google.com/books?id=e1KkHAAACAAJ},
  year={1930},
  publisher={De{\"u}tsche Akademie der Wissenschaften zu Berlin, Mathematisch-Naturwissenschaftliche Klasse}
}

@book{peano1889arithmetices,
  title={Arithmetices principia: nova methodo},
  author={Peano, Giuseppe},
  year={1889},
  publisher={Fratres Bocca}
}
@inproceedings{Werner:92,
author = {B. Werner},
title = {{A Normalization Proof for an Impredicative Type System with Large Elimination over Integers}},
booktitle="International Workshop on Types for Proofs and Programs (TYPES)",
year="1992",
editor={B. Nordstr\"om and K. Petersson and G. Plotkin},
note={The TYPES 1992 proceedings are available at \url{http://www.cse.chalmers.se/research/group/logic/Types/proc92.ps}.},
pages="341--357"}
@book{Girard:1989,
 author = {Girard, Jean-Yves and Taylor, Paul and Lafont, Yves},
 title = {Proofs and types},
 year = {1989},
 isbn = {0-521-37181-3},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
} 

@article{Stump:2009,
 author = {Stump, Aaron},
 title = {Directly reflective meta-programming},
 journal = {Higher Order Symbol. Comput.},
 issue_date = {June      2009},
 volume = {22},
 number = {2},
 month = jun,
 year = {2009},
 issn = {1388-3690},
 pages = {115--144},
 numpages = {30},
 url = {http://dx.doi.org/10.1007/s10990-007-9022-0},
 doi = {10.1007/s10990-007-9022-0},
 acmid = {1713772},
 publisher = {Kluwer Academic Publishers},
 address = {Hingham, MA, USA},
 keywords = {Alpha equivalence, Church encoding, Lambda calculus, reflection, Language implementation, Meta-programming, Mogensen-Scott encoding, Wand-style fexprs},
} 

@article{Barendregt:97,
  author    = {Henk Barendregt},
  title     = {The impact of the lambda calculus in logic and computer
               science},
  journal   = {Bulletin of Symbolic Logic},
  volume    = {3},
  number    = {2},
  year      = {1997},
  pages     = {181-215},
  ee        = {http://www.math.ucla.edu/$\sim$asl/bsl/0302/0302-003.ps},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@book{Winskel:1993,
 author = {Winskel, Glynn},
 title = {The formal semantics of programming languages: an introduction},
 year = {1993},
 isbn = {0-262-23169-7},
 publisher = {MIT Press},
 address = {Cambridge, MA, USA},
} 

@book{Pierce:2002,
 author = {Pierce, Benjamin C.},
 title = {Types and programming languages},
 year = {2002},
 isbn = {0-262-16209-1},
 publisher = {MIT Press},
 address = {Cambridge, MA, USA},
} 

@book{hindley1997basic,
  title={Basic simple type theory},
  author={Hindley, J Roger},
  volume={42},
  year={1997},
  publisher={Cambridge University Press}
}
@book{Barendregt:1985,
  title={The lambda calculus: Its syntax and semantics},
  author={Barendregt, Hendrik Pieter},
  volume={103},
  year={1985},
  publisher={North Holland}
}
@book{baader1999term,
  title={Term rewriting and all that},
  author={Baader, Franz and Nipkow, Tobias},
  year={1999},
  publisher={Cambridge University Press}
}
@article{Hardin:1989,
 author = {Hardin, Th{\'e}r\`{e}se},
 title = {Confluence results for the pure strong categorical logic CCL. $\lambda$-calculi as subsystems of CCL},
 journal = {Theor. Comput. Sci.},
 issue_date = {July 1989},
 volume = {65},
 number = {3},
 month = jul,
 year = {1989},
 issn = {0304-3975},
 pages = {291--342},
 numpages = {52},
 url = {http://dx.doi.org/10.1016/0304-3975(89)90105-9},
 doi = {10.1016/0304-3975(89)90105-9},
 acmid = {70103},
 publisher = {Elsevier Science Publishers Ltd.},
 address = {Essex, UK},
} 

@article{bezem2003term,
  title={Term rewriting systems. Terese},
  author={Bezem, Marc and Klop, Jan Willem and de Vrijer, Roel},
  year={2003},
  publisher={Cambridge Tracts in Theoretical Computer Science}
}
@misc{frege1967basic,
  title={The Basic Laws of Arithmetic: Exposition of the System, translated and edited with an introduction by Montgomery Furth},
  author={Frege, Gottlob},
  year={1967},
  publisher={University of California Press}
}
@book{frege1988grundlagen,
  title={Grundlagen der Arithmetik: Studienausgabe mit dem Text der Centenarausgabe},
  author={Frege, Gottlob},
  year={1988},
  publisher={Meiner Verlag}
}
@book{dowd2006art,
  title={The art of software security assessment: Identifying and preventing software vulnerabilities},
  author={Dowd, Mark and McDonald, John and Schuh, Justin},
  year={2006},
  publisher={Addison-Wesley Professional}
}
@article{von1993first,
  title={First Draft of a Report on the EDVAC},
  author={Von Neumann, John},
  journal={Annals of the History of Computing, IEEE},
  volume={15},
  number={4},
  pages={27--75},
  year={1993},
  publisher={IEEE}
}
@article{Gentzen:1964,
  title={Investigations into logical deduction},
  author={Gentzen, Gerhard},
  journal={American philosophical quarterly},
  volume={1},
  number={4},
  pages={288--306},
  year={1964},
  publisher={JSTOR}
}
@manuscript{abadi93,
title={{Types for the Scott Numerals}},
author={M. Abadi and L. Cardelli and G. Plotkin},
note="Unpublished, available from Abadi's web page",
year=1993,
pages={1--2}}                  

@article{Jansen:2011,
  author    = {J.M. Jansen and R. Plasmeijer and P. Koopman},
  title     = {Functional Pearl: Comprehensive Encoding of Data Types and Algorithms in the lambda-Calculus},
  journal   = {Internal report, NLDA},
  year      = {2011},
}


@article{Coq,
  title={The Coq Proof Assistant Reference Manual},
  author={The Coq Development Team},
  journal={Version 8.3. INRIA},
  publisher={Available from http://coq.inria.fr/V8.3/refman/},
  year={2010}
}
@incollection{McBride:2005,
year={2005},
isbn={978-3-540-28540-3},
booktitle={Advanced Functional Programming},
volume={3622},
series={Lecture Notes in Computer Science},
editor={Vene, Varmo and Uustalu, Tarmo},
doi={10.1007/11546382_3},
title={Epigram: Practical Programming with Dependent Types},
url={http://dx.doi.org/10.1007/11546382_3},
publisher={Springer Berlin Heidelberg},
author={McBride, Conor},
pages={130-170}
}

@article{Wright:1994,
  title={A syntactic approach to type soundness},
  author={Wright, Andrew K and Felleisen, Matthias},
  journal={Information and computation},
  volume={115},
  number={1},
  pages={38--94},
  year={1994},
  publisher={San Diego: Academic Press, c1987-}
}
@article{Pfenning:1988,
  title={Higher-order abstract syntax},
  author={Pfenning, Frank and Elliot, Conal},
  journal={ACM SIGPLAN Notices},
  volume={23},
  number={7},
  pages={199--208},
  year={1988},
  publisher={ACM}
}
@dissertation{Girard:72,
author="Jean-Yves Girard",
title="Interpr\'etation fonctionnelle et \'elimination des coupures de l'arithm\'etique d'ordre sup\'erieur",
institution="Universit\'e Paris VII",
year="1972"}
@article{Coquand:1988,
 author = {Coquand, Thierry and Huet, Gerard},
 title = {The calculus of constructions},
 journal = {Inf. Comput.},
 issue_date = {February/March 1988},
 volume = {76},
 number = {2-3},
 month = feb,
 year = {1988},
 issn = {0890-5401},
 pages = {95--120},
 numpages = {26},
 url = {http://dx.doi.org/10.1016/0890-5401(88)90005-3},
 doi = {10.1016/0890-5401(88)90005-3},
 acmid = {47725},
 publisher = {Academic Press, Inc.},
 address = {Duluth, MN, USA},
} 

@inproceedings{Coquand:1990,
  title={Inductively defined types},
  author={Coquand, Thierry and Paulin, Christine},
  booktitle={COLOG-88},
  pages={50--66},
  year={1990},
  organization={Springer}
}
@incollection{Paulin:1993,
  title={Inductive definitions in the system coq rules and properties},
  author={Paulin-Mohring, Christine},
  booktitle={Typed lambda calculi and applications},
  pages={328--345},
  year={1993},
  publisher={Springer}
}
@misc{gimenez2005tutorial,
  title={A tutorial on [co-] inductive types in coq},
  author={Gim{\'e}nez, Eduardo and Cast{\'e}ran, Pierre},
  year={2005}
}
@inproceedings{Stump:2009-2,
 author = {Stump, Aaron and Deters, Morgan and Petcher, Adam and Schiller, Todd and Simpson, Timothy},
 title = {Verified programming in Guru},
 booktitle = {Proceedings of the 3rd workshop on Programming languages meets program verification},
 series = {PLPV '09},
 year = {2008},
 isbn = {978-1-60558-330-3},
 location = {Savannah, GA, USA},
 pages = {49--58},
 numpages = {10},
 url = {http://doi.acm.org/10.1145/1481848.1481856},
 doi = {10.1145/1481848.1481856},
 acmid = {1481856},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {dependently typed programming, language-based verification, operational type theory},
} 

@incollection{Bove:2009,
  title={A brief overview of Agda--a functional language with dependent types},
  author={Bove, Ana and Dybjer, Peter and Norell, Ulf},
  booktitle={Theorem Proving in Higher Order Logics},
  pages={73--78},
  year={2009},
  publisher={Springer}
}
@phdthesis{vaninwegen1996machine,
  title={The machine-assisted proof of programming language properties},
  author={VanInwegen, Myra},
  year={1996},
  school={University of Pennsylvania}
}
@inproceedings{Gregoire:2010,
  title={On strong normalization of the calculus of constructions with type-based termination},
  author={Gr{\'e}goire, Benjamin and Sacchini, Jorge Luis},
  booktitle={Logic for Programming, Artificial Intelligence, and Reasoning},
  pages={333--347},
  year={2010},
  organization={Springer}
}
@incollection{aydemir2005mechanized,
  title={Mechanized metatheory for the masses: The POPLmark challenge},
  author={Aydemir, Brian E and Bohannon, Aaron and Fairbairn, Matthew and Foster, J Nathan and Pierce, Benjamin C and Sewell, Peter and Vytiniotis, Dimitrios and Washburn, Geoffrey and Weirich, Stephanie and Zdancewic, Steve},
  booktitle={Theorem Proving in Higher Order Logics},
  pages={50--65},
  year={2005},
  publisher={Springer}
}
@article{Milner:1997,
  title={The Definition of Standard ML, revised edition},
  author={Milner, Robin and Tofte, Mads and Harper, Robert and MacQueen, David},
  journal={MIT Press},
  volume={1},
  number={2},
  pages={2--3},
  year={1997}
}
@book{martin:1984,
  title={Intuitionistic type theory},
  author={Martin-L\"of, Per and Sambin, Giovanni},
  volume={17},
  year={1984},
  publisher={Bibliopolis Naples,, Italy}
}
@article{Howard:1980,
  title={The formulae-as-types notion of construction},
  author={Howard, William A},
  journal={To HB Curry: essays on combinatory logic, lambda calculus and formalism},
  volume={44},
  pages={479--490},
  year={1980}
}
@book{CHS:72,
  author = {H. B. Curry and J. R. Hindley and J. P. Seldin},
  title = {Combinatory Logic, Volume II},
  publisher = {North-Holland},
  year = {1972},
  pages = {xiv+520}
}
@article{Ariola:1997,
title = "Lambda Calculus with Explicit Recursion ",
journal = "Information and Computation ",
volume = "139",
number = "2",
pages = "154 - 233",
year = "1997",
note = "",
issn = "0890-5401",
doi = "10.1006/inco.1997.2651",
url = "http://www.sciencedirect.com/science/article/pii/S0890540197926511",
author = "Zena M. Ariola and Jan Willem Klop"
}


@article{CurienHL96,
  author    = {Pierre-Louis Curien and
               Th{\'e}r{\`e}se Hardin and
               Jean-Jacques L{\'e}vy},
  title     = {Confluence Properties of Weak and Strong Calculi of Explicit
               Substitutions},
  journal   = {J. ACM},
  volume    = {43},
  number    = {2},
  year      = {1996},
  pages     = {362-397},
  ee        = {http://doi.acm.org/10.1145/226643.226675},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{Takahashi95,
  author    = {Masako Takahashi},
  title     = {Parallel Reductions in lambda-Calculus},
  journal   = {Inf. Comput.},
  volume    = {118},
  number    = {1},
  year      = {1995},
  pages     = {120-127},
  ee        = {http://dx.doi.org/10.1006/inco.1995.1057},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@InCollection{sep-identity-indiscernible,
	author       =	{Forrest, Peter},
	title        =	{The Identity of Indiscernibles},
	booktitle    =	{The Stanford Encyclopedia of Philosophy},
	editor       =	{Edward N. Zalta},
	howpublished =	{\url{http://plato.stanford.edu/archives/win2012/entries/identity-indiscernible/}},
	year         =	{2012},
	edition      =	{Winter 2012},
}

@INPROCEEDINGS{Barendregt:92,
    author = {Henk Barendregt and S. Abramsky and D. M. Gabbay and T. S. E. Maibaum and H. P. Barendregt},
    title = {Lambda Calculi with Types},
    booktitle = {Handbook of Logic in Computer Science},
    year = {1992},
    pages = {117--309},
    publisher = {Oxford University Press}
}

@techreport{coquand:inria-00075471,
    hal_id = {inria-00075471},
    url = {http://hal.inria.fr/inria-00075471},
    title = {{Metamathematical investigations of a calculus of constructions}},
    author = {Coquand, T.},
    language = {English},
    affiliation = {INRIA Rocquencourt - INRIA Rocquencourt},
    institution = {INRIA},
    number = {RR-1088},
    year = {1989},
    month = Sep,
    pdf = {http://hal.inria.fr/inria-00075471/PDF/RR-1088.pdf},
}
@inproceedings{Geuvers:2001,
 author = {Geuvers, Herman},
 title = {Induction is not derivable in second order dependent type theory},
 booktitle = {Proceedings of the 5th international conference on Typed lambda calculi and applications},
 series = {TLCA'01},
 year = {2001},
 isbn = {3-540-41960-8},
 location = {Krak\&\#243;w, Poland},
 pages = {166--181},
 numpages = {16},
 url = {http://dl.acm.org/citation.cfm?id=1754621.1754639},
 acmid = {1754639},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
} 


@book{Barendregt85,
    author = {Barendregt, H. P.},
    edition = {Revised},
    howpublished = {Paperback},
    isbn = {0444875085},
    keywords = {lambda},
    month = nov,
    posted-at = {2006-08-20 10:51:05},
    priority = {0},
    publisher = {North Holland},
    title = {{The Lambda Calculus, Its Syntax and Semantics (Studies in Logic and the Foundations of Mathematics, Volume 103). Revised Edition}},
    year = {1985}
}
